fpf{-}normalize(${\it eq}$;$g$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$reduce($\lambda$$x$,$f$. $x$ : 2of($g$)($x$) $\oplus$ $f$;;1of($g$))